\begin{tad}{TABLERO}
\\
\hrule

\generadores
	\func{dados}  {nat/d1, nat/d2}{dados}  {}
  \func{Tablero}{secu(casilla)} {tablero}{cardinal(secu) mod 4 = 0 $\land$ hayCarcel(s) $\land$ hayInicio(s))}

\observadores
  \func{Casillas}{tablero}{secu(casilla)}{}
	\func{sonIguales}{dados}{bool}{}
	\func{Suma}      {dados}{nat} {}


\otrasops
  \func{enesimoT}{tablero/t x nat/n}{casilla}{}
  \func{hayCarcel}{secu(casilla)/sc}{Bool}{}
  \func{HayInicio}{secu(casilla)/sc}{Bool}{}

\axiomas{($\forall$ sc:secu(casilla))}
	\axioma{Casillas(tablero(s))}{s}
	\axioma{enesimoT (t)}{enesimo(casillas(t))}
	\axioma{hayCarcel? (<>)}{False}
	\axioma{HayCarcel? (a.s)}{(esCarcel?(a) $\implies$ $\neg$HayCarcel?(s)) $\land$ \\ 
	                          $\neg$esCarcel?(a) $\implies$ HayCarcel?(s)}
	\axioma{hayInicio? (<>)}{False}
	\axioma{HayInicio? (a.s)}{(esInicio?(a) $\implies$ $\neg$HayInicio?(s)) $\land$ \\ 
	                          $\neg$esInicio?(a) $\implies$ HayInicio?(s)}
\end{tad}

